Termination Proof Script

Consider the TRS R consisting of the rewrite rules

There are 5 dependency pairs:

The approximated dependency graph contains one SCC: {3-7}.

Consider the SCC {3-7}. By taking the AF π with π(PLUS) = 2 and π(plus) = [2] together with the lexicographic path order with empty precedence, the rules in {1-3,5} are weakly decreasing and the rules in {4,6,7} are strictly decreasing. There is one new SCC.
- Consider the SCC {3,5}. By taking the AF π with π(plus) = π(PLUS) = 1 together with the lexicographic path order with empty precedence, the rules in {1-3,5} are strictly decreasing.

Hence the TRS is terminating.

Tyrolean Termination Tool (0.01 seconds) --- May 3, 2006